MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { #equal(@x, @y) -> #eq(@x, @y)
  , appendreverse(@toreverse, @sofar) ->
    appendreverse#1(@toreverse, @sofar)
  , appendreverse#1(::(@a, @as), @sofar) ->
    appendreverse(@as, ::(@a, @sofar))
  , appendreverse#1(nil(), @sofar) -> @sofar
  , bfs(@queue, @futurequeue, @x) -> bfs#1(@queue, @futurequeue, @x)
  , bfs#1(::(@t, @ts), @futurequeue, @x) ->
    bfs#3(@t, @futurequeue, @ts, @x)
  , bfs#1(nil(), @futurequeue, @x) -> bfs#2(@futurequeue, @x)
  , bfs#3(leaf(), @futurequeue, @ts, @x) ->
    bfs(@ts, @futurequeue, @x)
  , bfs#3(node(@y, @t1, @t2), @futurequeue, @ts, @x) ->
    bfs#4(#equal(@x, @y), @futurequeue, @t1, @t2, @ts, @x, @y)
  , bfs#2(::(@t, @ts), @x) -> bfs(reverse(::(@t, @ts)), nil(), @x)
  , bfs#2(nil(), @x) -> leaf()
  , reverse(@xs) -> appendreverse(@xs, nil())
  , bfs#4(#false(), @futurequeue, @t1, @t2, @ts, @x, @y) ->
    bfs(@ts, ::(@t2, ::(@t1, @futurequeue)), @x)
  , bfs#4(#true(), @futurequeue, @t1, @t2, @ts, @x, @y) ->
    node(@y, @t1, @t2)
  , bfs2(@t, @x) -> bfs2#1(dobfs(@t, @x), @x)
  , dobfs(@t, @x) -> bfs(::(@t, nil()), nil(), @x)
  , bfs2#1(@t', @x) -> dobfs(@t', @x)
  , dfs(@queue, @x) -> dfs#1(@queue, @x)
  , dfs#1(::(@t, @ts), @x) -> dfs#2(@t, @t, @ts, @x)
  , dfs#1(nil(), @x) -> leaf()
  , dfs#2(leaf(), @t, @ts, @x) -> dfs(@ts, @x)
  , dfs#2(node(@a, @t1, @t2), @t, @ts, @x) ->
    dfs#3(#equal(@a, @x), @t, @t1, @t2, @ts, @x)
  , dfs#3(#false(), @t, @t1, @t2, @ts, @x) ->
    dfs(::(@t1, ::(@t2, @ts)), @x)
  , dfs#3(#true(), @t, @t1, @t2, @ts, @x) -> @t
  , dodfs(@t, @x) -> dfs(::(@t, nil()), @x) }
Weak Trs:
  { #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
    #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
  , #eq(::(@x_1, @x_2), nil()) -> #false()
  , #eq(::(@x_1, @x_2), leaf()) -> #false()
  , #eq(::(@x_1, @x_2), node(@y_1, @y_2, @y_3)) -> #false()
  , #eq(nil(), ::(@y_1, @y_2)) -> #false()
  , #eq(nil(), nil()) -> #true()
  , #eq(nil(), leaf()) -> #false()
  , #eq(nil(), node(@y_1, @y_2, @y_3)) -> #false()
  , #eq(leaf(), ::(@y_1, @y_2)) -> #false()
  , #eq(leaf(), nil()) -> #false()
  , #eq(leaf(), leaf()) -> #true()
  , #eq(leaf(), node(@y_1, @y_2, @y_3)) -> #false()
  , #eq(node(@x_1, @x_2, @x_3), ::(@y_1, @y_2)) -> #false()
  , #eq(node(@x_1, @x_2, @x_3), nil()) -> #false()
  , #eq(node(@x_1, @x_2, @x_3), leaf()) -> #false()
  , #eq(node(@x_1, @x_2, @x_3), node(@y_1, @y_2, @y_3)) ->
    #and(#eq(@x_1, @y_1), #and(#eq(@x_2, @y_2), #eq(@x_3, @y_3)))
  , #eq(#0(), #0()) -> #true()
  , #eq(#0(), #neg(@y)) -> #false()
  , #eq(#0(), #pos(@y)) -> #false()
  , #eq(#0(), #s(@y)) -> #false()
  , #eq(#neg(@x), #0()) -> #false()
  , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
  , #eq(#neg(@x), #pos(@y)) -> #false()
  , #eq(#pos(@x), #0()) -> #false()
  , #eq(#pos(@x), #neg(@y)) -> #false()
  , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
  , #eq(#s(@x), #0()) -> #false()
  , #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
  , #and(#false(), #false()) -> #false()
  , #and(#false(), #true()) -> #false()
  , #and(#true(), #false()) -> #false()
  , #and(#true(), #true()) -> #true() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'Fastest' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'custom shape polynomial interpretation' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   2) 'custom shape polynomial interpretation' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'linear polynomial interpretation' failed due to the following
      reason:
      
      The input cannot be shown compatible
   

2) 'Fastest' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'matrix interpretation of dimension 4' failed due to the
      following reason:
      
      Following exception was raised:
        stack overflow
   
   2) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   4) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   5) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   6) 'matrix interpretation of dimension 1' failed due to the
      following reason:
      
      The input cannot be shown compatible
   


Arrrr..